\begin{tabbing}
F2F+{-}decls
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it is\_req}$:(E$\rightarrow\mathbb{P}$)\+
\\[0ex]$\times$ (${\it is\_ack}$:(E$\rightarrow\mathbb{P}$)
\\[0ex]$\times$ ${\it awaiting}$:(Id$\rightarrow$Id$\rightarrow$Id)
\\[0ex]$\times$ ${\it owes\_ack}$:(Id$\rightarrow$Id$\rightarrow$Id)
\\[0ex]$\times$ ${\it C\_sub\_Id}$:(${\it ff}$.C $\subseteq$r Id)
\\[0ex]$\times$ ${\it vbl\_locs}$:($\forall$$i$, $j$:${\it ff}$.C. @$i$(${\it awaiting}$($i$,$j$):$\mathbb{B}$) \& @$i$(${\it owes\_ack}$($i$,$j$):$\mathbb{B}$))
\\[0ex]$\times$ ${\it R\_locs}$:($\forall$$i$:${\it ff}$.C, $e$:E. (${\it ff}$.R($i$,$e$)) $\Rightarrow$ (loc($e$) = $i$))
\\[0ex]$\times$ ${\it req\_dcdr}$:($\forall$$e$:E. Dec(${\it is\_req}$($e$)))
\\[0ex]$\times$ ${\it ack\_dcdr}$:($\forall$$e$:E. Dec(${\it is\_ack}$($e$)))
\\[0ex]$\times$ ${\it R\_dcdr}$:($\forall$$i$:${\it ff}$.C, $e$:E. Dec(${\it ff}$.R($i$,$e$)))
\\[0ex]$\times$ ${\it S\_dcdr}$:($\forall$$i$, $j$:${\it ff}$.C, $e$:E. Dec(${\it ff}$.S($i$,$j$,$e$)))
\\[0ex]$\times$ ${\it S\_locs}$:($\forall$$i$, $j$:${\it ff}$.C, $e$:E. (${\it ff}$.S($i$,$j$,$e$)) $\Rightarrow$ (loc($e$) = $i$))
\\[0ex]$\times$ (${\it disjoint\_msgs}$:\=($\forall$$e$:E, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C.\+
\\[0ex]$\neg$([$e$: ${\it sndr}$ $--$${\it is\_req}$$\rightarrow$ ${\it rcvr}$] \& [$e$: ${\it rcvr}$ $--$${\it is\_ack}$$\rightarrow$ ${\it sndr}$]))
\-\\[0ex]$\times$ Top))
\-
\end{tabbing}